X:Type, eq:EqDecider(X), f, g:x:X fp Type, x:X.
f || g  f(x)?Void  g(x)?Void  (f(x)?Void = g(x)?Void  Type) 

latex

Definitions	x:A. B(x), P  Q, t  T, x. t(x), f(x)?z, if b then t else f fi , tt, ff, , P & Q, x(s), , Unit, P  Q, f || g,
Lemmas	fpf-compatible wf, fpf wf, deq wf, fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot